perm filename MARS[1,JRA] blob sn#005883 filedate 1972-10-20 generic text, type T, neo UTF8
00020	A1: x/y ≤ x ;
00050	
00100	DEF_OF_LESS: x ≤ y ≡ x/y = 0;
00300	A2: (x/z) /(y/z) ≤  (x/y)/z ;
00400	A3: 0 ≤ x ;
00500	
00600	A4: x ≤ y ∧ y ≤ x ⊃ x = y;
00700	A5: x ≤ 1; 
00800	 ;